COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 00003
C00006 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.TURN ON "↑"
.bb Expressing theorems about recursion in set theory.

	The object of these notes is to explore the possibility of doing
program correctness proofs in set theory beginning with the basic
theorems on the existence and properties of recursive functions.

	Halmos (1960) proves the following "recursion theorem".

!!a1:	%2∀a g X.aεX ∧ gεX↑X ⊃ ∃f.fεX↑qw ∧ f(0) = a ∧ ∀n.nεqw ⊃ f(n') = g(f(n))%1.

	In a LISP-like language ⊗f would be defined recursively by

!!a3:	%2f(n) ← qif n = 0 qthen a qelse g(f(n-1))%1.

The following are alternative definitions of ⊗f: 

!!a5:	%2f = α{u ε qwqxX|∀z.((<0,a> ε z ∧ ∀n x.(<n,x> ε z ⊃ <n',g(x)> ε z))
⊃ u ε z)α}%1

and

!!a6:	%2f = %8∩%2α{z ε P(qw qx X)|<0,a> ε z ∧ ∀n.(<n,x> ε z ⊃ <n',g(x)> ε z)α}
%1.

We must then prove

!!a7:	%2∀n.∃!x.(<n,x> ε f)%1

and

!!a8:	%2∀n x.(<n,x> ε f ≡ (n=0 ∧ x=a ∨ n≠0 ∧ ∃x1.(<n-1,x1> ε f ∧ x = g(x1))))
%1.

	There is a direct generalization of ({eq a1}) which does
not presuppose the existence of the set ⊗X, namely

!!a2:	%2∀x ∃!y.P(x,y) ⊃ ∀a.∃X f.aεX ∧ fεX↑qw ∧ f(0) = a ∧ ∀n.(nεqw ⊃
P(f(n),f(n')))%1.

	The proof of ({eq a2}) uses quite a bit of set theoretic machinery
and is worth studying, because we will need the machinery later.

References:

%3Halmos, Paul R.%1 (1960) %2Naive Set Theory%1